\begin{tabbing}
$\forall$\=$i$:Id, $k$:Knd, $l$:IdLnk, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$a$:Knd fp$\rightarrow$ Type,\+
\\[0ex]$f$:((${\it tg}$:Id $\times$ (State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$(${\it da}$(rcv($l$,${\it tg}$))?Void List))) List).
\-\\[0ex](source($l$) = $i$)
\\[0ex]$\Rightarrow$ \=@$i$: with declarations \+
\\[0ex]ds:${\it ds}$
\\[0ex]d\=a:${\it da}$\+
\\[0ex]$k$(v) sends $f$ s v on link $l$ 
\-\\[0ex]realizes ${\it es}$.
\\[0ex](($\forall$$x$:Id. vartype($i$;$x$) $\subseteq$r ${\it ds}$($x$)?Top)
\\[0ex]\& ($\forall$$e$:E. (loc($e$) = $i$ $\in$ Id) $\Rightarrow$ (valtype($e$) $\subseteq$r Valtype(${\it da}$;kind($e$))))
\\[0ex]\& ($\forall$$e$:E. ($\uparrow$isrcv($e$)) $\Rightarrow$ (lnk($e$) = $l$ $\in$ IdLnk) $\Rightarrow$ (valtype($e$) $\subseteq$r Valtype(${\it da}$;kind($e$)))))
\\[0ex]c$\wedge$ \=($\forall$$e$:E.\+
\\[0ex](loc($e$) = $i$ $\in$ Id)
\\[0ex]$\Rightarrow$ (kind($e$) = $k$ $\in$ Knd)
\\[0ex]$\Rightarrow$ ($\exists$\=$L$:\{${\it e'}$:E$\mid$ ($\uparrow$isrcv(${\it e'}$)) c$\wedge$ (lnk(${\it e'}$) = $l$ $\in$ IdLnk)\}  List\+
\\[0ex]((\=$\forall$${\it e'}$:E.\+
\\[0ex](${\it e'}$ $\in$ $L$) $\Leftarrow\!\Rightarrow$ (($\uparrow$isrcv(${\it e'}$)) c$\wedge$ (lnk(${\it e'}$) = $l$ $\in$ IdLnk \& sender(${\it e'}$) = $e$ $\in$ E)))
\-\\[0ex]\& ($\forall$$e_{1}$, $e_{2}$:E. $e_{1}$ before $e_{2}$ $\in$ $L$ $\Rightarrow$ ($e_{1}$ $<$loc $e_{2}$))
\\[0ex]\& \=map($\lambda$${\it e'}$.$<$tag(${\it e'}$), val(${\it e'}$)$>$;$L$)\+
\\[0ex]=
\\[0ex]tagged{-}list{-}messages($\lambda$$z$.$z$ when $e$;val($e$);$f$)
\\[0ex]$\in$ ((${\it tg}$:Id $\times$ Valtype(${\it da}$;rcv($l$,${\it tg}$))) List))))
\-\-\-\-
\end{tabbing}